 // Atomic Proposition p0 = ((signal_delta23 > 1 && ! signal_valid1) -> (signal_mismatch1))
extern "C" bool prop_p0( divine::SMTRep *smt, bool neg ) {
  divine::Expr e( smt );
  uint32_t c = 0;
  divine::Node notN( divine::OP, divine::NOT, 1, c+1, 0 );
  if ( neg ) {
    e.nodes.push_back( notN );
    c++;
  }
  divine::Node impN( divine::OP, divine::IMP, 2, c+1, c+2 );
  c+=2;
  e.nodes.push_back( impN );
  divine::Node andN( divine::OP, divine::AND, 2, c+1, c+2 );
  c+=2;
  e.nodes.push_back( andN );
  divine::Node vN( divine::VAR, smt->by_name( "signal_mismatch1" ) );
  e.nodes.push_back( vN );
  divine::Node gtN( divine::OP, divine::GT, 2, c+1, c+2 );
  c+=2;
  e.nodes.push_back( gtN );
  divine::Node notN2( divine::OP, divine::NOT, 1, c+1, 0 );
  e.nodes.push_back( notN2 );
  divine::Node vN2( divine::VAR, smt->by_name( "signal_delta23" ) );
  e.nodes.push_back( vN2 );
  divine::Node cN( divine::CON, 1 );
  e.nodes.push_back( cN );
  divine::Node vN3( divine::VAR, smt->by_name( "signal_valid1" ) );
  e.nodes.push_back( vN3 );

  smt->addToPath( &e );
  bool retVal = smt->pc_sat( false );
  //std::cout << retVal << std::endl;//debug
  return retVal;
}

 // Atomic Proposition q1 = (permanent_mismatch1)
extern "C" bool prop_q1( divine::SMTRep *smt, bool neg ) {
  divine::Expr e( smt );
  divine::Node notN( divine::OP, divine::NOT, 1, 1, 0 );
  if ( neg ) {
    e.nodes.push_back( notN );
  }
  divine::Node vN( divine::VAR, smt->by_name( "permanent_mismatch1" ) );
  e.nodes.push_back( vN );
  smt->addToPath( &e );
  return smt->pc_sat( false );
}

 // Atomic Proposition p1 = (permanent_mismatch1)
extern "C" bool prop_p1( divine::SMTRep *smt, bool neg ) {
  return prop_q1( smt, neg );
}

 // Atomic Proposition p2 = (signal_mismatch1)
extern "C" bool prop_p2( divine::SMTRep *smt, bool neg ) {
  divine::Expr e( smt );
  divine::Node notN( divine::OP, divine::NOT, 1, 1, 0 );
  if ( neg ) {
    e.nodes.push_back( notN );
  }
  divine::Node vN( divine::VAR, smt->by_name( "signal_mismatch1" ) );
  e.nodes.push_back( vN );
  smt->addToPath( &e );
  return smt->pc_sat( false );
}

 // Atomic Proposition s2 = (permanent_mismatch1)
extern "C" bool prop_s2( divine::SMTRep *smt, bool neg ) {
  return prop_q1( smt, neg );
}
